It seems to me like the module case should be made to work rather than prevented. What do you think? I think it's fine to prevent it as a short term solution, but I want to make sure that this is being done deliberately.

It seems to me like the module case should be made to work rather than prevented. What do you think? I think it's fine to prevent it as a short term solution, but I want to make sure that this is being done deliberately.

Currently, the code does not generalise declared module in modules. So the check should be fixed w.r.t. that behaviour. Then, we can have a subsequent feature request for this.

This change is breaking some of my EasyUC proofs.

Actually, I seem to have left out a local. I'll report back.

Yes, false alarm. All good from my end.